COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(proof AXIOMS)
C00016 ENDMK
C⊗;
(proof AXIOMS)
(DECL (X Y Z X1 X2 X3 Y1 Y2 Y3 Z1 Z2 Z3) |GROUND| VARIABLE SEXP)
(DECL (A B C A1 A2 B1 B2 C1 C2) |GROUND| VARIABLE ATOM)
(DECL (TT NNIL) |GROUND| CONSTANT ATOM)
(DECL (G G1 G2 G3) |GROUND| VARIABLE)
(DECL (CAR CDR) |GROUND→GROUND| CONSTANT)

(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)
(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)
(AXIOM |∀G.ATOM(G)⊃SEXP(G)|)
(AXIOM |∀X Y.SEXP(CONS(X,Y))|)
(AXIOM |∀G.SEXP(G)⊃ATOM(G)∨(∃X Y.G=CONS(X,Y))|)

(AXIOM |∀X Y.¬ATOM(CONS(X,Y))|)
(AXIOM |∀X Y.CAR(CONS(X,Y))=X|)
(AXIOM |∀X Y.CDR(CONS(X,Y))=Y|)
(AXIOM |∀PHI.∀A.PHI(A)∧(∀X Y.(PHI(X)∧PHI(Y)⊃PHI(CONS(X,Y)))⊃(∀X.PHI(X)))|)
(DECL (U V W U1 U2 U3 V1 V2 V3 W1 W2 W3) |GROUND| VARIABLE LIST)

(DECL (NULL) |GROUND→TRUTHVAL|)
(AXIOM |NULL(NNIL)|)
(AXIOM |∀U.NULL(U)≡U=NNIL|)
(AXIOM |LIST(NNIL)|)
(AXIOM |∀G.LIST(G)⊃SEXP(G)|)

(AXIOM |∀X U.¬NULL(CONS(X,U))|)
(AXIOM |∀X U.LIST(CONS(X,U))|)
(AXIOM |∀U.¬NULL(U)⊃(∃X U1.U=CONS(X,U1))|)
(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))|)

;(assume |∀x u.car(cons(x,u))=x|)
;(rw 22 der 20 12)
;(DECIDE |∀X U.CDR(CONS(X,U))=U| 20 13)